ds:(IdType), da:(IdKndType), A, B:Type.
(A r B)  (Interface(ds;da;A) r Interface(ds;da;B)) 

latex

Definitions	Interface(ds;da;A), a:A fp B(a), type List, x. t(x), P  Q, x.A(x), x,y. t(x;y), f(a), left + right, Top, Knd, Type, b, hasloc(k;i), Id, x:AB(x), let i,k:LocKnd = ik in P(i;k), (x  l), x:A. B(x), t  T, LocKnd, {x:A| B(x)} , x:A  B(x), s = t, <a, b>, Atom$n
Lemmas	subtype rel sum, subtype rel function, LocKnd wf, l member wf, subtype rel self, Id wf, hasloc wf, assert wf, Knd wf, top wf, locknd-spread wf2, subtype rel dep function, subtype rel product